M:MsgA. ma-is-empty(M)   

latex

Definitions	t  T, Id, x:A. B(x), ||as||, i=j, Knd, IdLnk, a:A fp B(a), Top, fpf-is-empty(f), , p  q, ma-is-empty(M), MsgA
Lemmas	msga wf, band wf, IdLnk wf, Knd wf, eq int wf, length wf1, Id wf